Fix BMC token-extract fail-open: jq -r '.token // empty' makes a missing token an empty file reported Converged (gunbc.host_effect_realize realize_bmcweb_token_extract_body); sweep the jq -e class - #8454

… split rung

Four load-bearing corrections found by review, two of which were errors in the
first revision.

1. jq exit decoding is POLICY-INDEXED, not universal. Verified against
   jqlang.org/manual: default jq exits 0 regardless of output, and only
   --exit-status yields 1 (last result false/null) and 4 (no valid result ever
   produced). The first revision put JqProducedNoResult as a general arm, which
   claims a distinction JqProgramExit cannot supply -- and would have
   reintroduced the exact Absent -> Refused collapse #8454 withdrew.
   SensorIntegerValue derives Absent from successful empty stdout under
   JqProgramExit, never from a jq exit code.

2. No generic decode_exactly_one_nonempty_string. jq emits a stream and -r
   permits newlines inside a raw string, so collapsed stdout is ambiguous;
   --raw-output0 exists for exactly that reason. The note now promises only
   "nonempty observed stdout" until a framing lands.

3. The CLI tree is SEALED. CliOption { values: List<_> } freely constructible
   admits wrong arity, non-repeatable options twice, foreign-tool options.
   Rows carry arity, repeatability, placement and joining; the emitter accepts
   only an admitted tree; domain callers hold no constructor for
   AdmittedCliOptionUse.

4. The rung was too coarse, and stating one number for two subjects was the
   error. The migrated jq path can reach STRUCTURALLY GUARANTEED now via
   sole_constructor + admit_callers -- the wall that closed TransportScript.
   The corpus at large stays mechanically preventable while 575 raw argv lines
   remain. The wall is the sealed constructor, not the type name.

Also: ownership splits by what fact a program encodes, so only policy-bearing
fan programs move to gunbc.bmc_fan_projection while OpenBMC wire decoders stay
in extdeps.bmc; stdin/env/cwd/fd belong to the process plan, not CliSyntax;
generalizing extdeps.posix Command is not a prerequisite, one narrow local jq
realization with an explicit dissolution trigger is; SensorIntegerValue named
as the canonical first vertical with slices B-D after it.

New open question, stated as risk not defect: the 17 remote jq rows place the
filter after the SSH destination as though its local argv boundary survived,
but ssh joins words into RFC 4254's single command string and sshd re-parses
through a login shell. Those filters carry pipes and quotes. Unverified -- no
executed control -- and must be settled before Slice D.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Two conflicts, both on srv3 actuation files main rewrote for the jq
fail-open sweep. Resolved to main's content whole, then this branch's
standing rule applied to what came in: the witness file arrived with three
import blocks, stripped, and its seven names qualified.

… boundaries survive the grammar fold, proven by execution) (#8467)

* CLI invocation emission design note: the tree is the authority, argv is emitted

Design-note-first, no code. Supersedes the Lane B destination of
gunbc.plans.transport_argv_anemia_dissolution, whose diagnosis stands but
which terminates at typed extdeps/tools/* operations and ArgvCommand
builders -- both of which still contain literal argv, so it stops one layer
short.

Measured census (the plan's own numbers are stale by ~2.3x): 597 argv lines
across 129 files, 250 transport shell blocks, 173 operations still carrying
success: Bool from exit_success against 69 preserving exit_code. 78 of 282
literal argv heads are wrappers rather than tools, so tool identity is a
positional accident and the corpus cannot currently be censused for what it
invokes.

The model: JqInvocation (semantic axes) -> CliInvocationTree (options grouped
with their values) -> List<PosixArgument> -> extdeps.posix Command, with the
SSH leg going through the shell grammar already grounded by
extdeps.posix.shell_command_language. Two-level row derivation is the
keystone: semantic property -> option row prevents omission, option row ->
spelling prevents bespoke spelling. Centralizing 597 literals into N helper
functions fixes neither.

Records what measurement refuted during design, including three of my own
claims, so they are not re-derived: the declarative form is not fixed-arity;
RFC 4254 forces a string at the SSH boundary; ProcessInvocation is an
emit-harness carrier, not the general one; SensorIntegerValue is live and its
empty-output branch is a modeled OpenBmcSensorValueAbsent, so an -e sweep
would have collapsed a correct three-state decode.

Rung stated honestly: mechanically preventable, not structural. 04_infer does
not typecheck application argument types, so a nominal CliArgument newtype
makes nothing unwritable today.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Design note corrections: policy-indexed jq decoding, sealed CLI tree, split rung

Four load-bearing corrections found by review, two of which were errors in the
first revision.

1. jq exit decoding is POLICY-INDEXED, not universal. Verified against
   jqlang.org/manual: default jq exits 0 regardless of output, and only
   --exit-status yields 1 (last result false/null) and 4 (no valid result ever
   produced). The first revision put JqProducedNoResult as a general arm, which
   claims a distinction JqProgramExit cannot supply -- and would have
   reintroduced the exact Absent -> Refused collapse #8454 withdrew.
   SensorIntegerValue derives Absent from successful empty stdout under
   JqProgramExit, never from a jq exit code.

2. No generic decode_exactly_one_nonempty_string. jq emits a stream and -r
   permits newlines inside a raw string, so collapsed stdout is ambiguous;
   --raw-output0 exists for exactly that reason. The note now promises only
   "nonempty observed stdout" until a framing lands.

3. The CLI tree is SEALED. CliOption { values: List<_> } freely constructible
   admits wrong arity, non-repeatable options twice, foreign-tool options.
   Rows carry arity, repeatability, placement and joining; the emitter accepts
   only an admitted tree; domain callers hold no constructor for
   AdmittedCliOptionUse.

4. The rung was too coarse, and stating one number for two subjects was the
   error. The migrated jq path can reach STRUCTURALLY GUARANTEED now via
   sole_constructor + admit_callers -- the wall that closed TransportScript.
   The corpus at large stays mechanically preventable while 575 raw argv lines
   remain. The wall is the sealed constructor, not the type name.

Also: ownership splits by what fact a program encodes, so only policy-bearing
fan programs move to gunbc.bmc_fan_projection while OpenBMC wire decoders stay
in extdeps.bmc; stdin/env/cwd/fd belong to the process plan, not CliSyntax;
generalizing extdeps.posix Command is not a prerequisite, one narrow local jq
realization with an explicit dissolution trigger is; SensorIntegerValue named
as the canonical first vertical with slices B-D after it.

New open question, stated as risk not defect: the 17 remote jq rows place the
filter after the SSH destination as though its local argv boundary survived,
but ssh joins words into RFC 4254's single command string and sshd re-parses
through a login shell. Those filters carry pipes and quotes. Unverified -- no
executed control -- and must be settled before Slice D.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Design note: orthogonal observation axes, sealed carriers, subject-grained rung, executing probe

Six corrections from review, four of them defects in my own prior revisions.

1. Termination and output presence are ORTHOGONAL, not a coproduct. The live
   SensorIntegerValue case holds exit 0 AND zero results simultaneously, so
   writing JqProducedNoResult as an arm beside JqExitZero makes the live case
   unrepresentable. Split into JqExitDisposition x JqOutputPresence.

2. Removing success: Bool was insufficient. An unsealed JqObservation still
   admits { exit: JqExitZero, exit_code: 4 } -- the same writable contradiction
   under richer names. JqObservation is now sole_constructor, minted only by the
   policy-aware decoder, with the raw process observation retained as evidence
   and decoded facts bound to it.

3. The rung sentence was internally inconsistent: "mechanically preventable
   because nothing refuses it" -- if nothing refuses it, it is not prevented.
   Replaced with a subject-grained matrix. The migrated path reaches
   structurally impossible NOW via sole_constructor; the corpus-wide raw-jq and
   raw-argv classes stay open. The terminal trigger is a DOMINATOR condition
   over jq execution paths, not application-argument typechecking, which is
   neither necessary for sealing this path nor sufficient against alternate
   raw routes.

4. Option spelling had two authorities -- jq "how it spells them" and CliSyntax
   "canonical spelling" -- committed inside a note about that exact violation.
   Tool row owns which forms exist and which is canonical; grammar owns how a
   chosen form is constructed.

5. The carrier probe will NOT refuse, so a compile-only probe false-greens.
   emit/serialize_target are fixed to Medium<String>, and v1.04_infer
   explicit_return_conformance_note records conformance is judged only by the
   ground-kernel-scalar and ground-element-collection discipline -- a structured
   Medium<String> vs Medium<CliSurface> mismatch is outside it. The probe is now
   an EXECUTING sibling-serializer probe with five controls, and does not begin
   by genericizing TargetModel.

6. The smallest complete vertical is LOCAL ONLY. SSH adds a second language
   target, RFC 4254 string loss, portable-word refusal, quoting and the sshpass
   -d 0 collision. Recut: Wave 0 probe, Wave 1A ObjectMapperServiceAt as the
   feature-rich exemplar, Wave 1B SensorIntegerValue as the required falsifier
   proving JqProgramExit selects no -e and absence is not refusal, Wave 2 SSH.

Also: the CLI inverse is partial and ambiguity-aware, answering
CliParseUnique | CliParseAmbiguous | CliParseRefused, and is not a Wave 1
acceptance criterion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Remote jq argument-boundary loss is source-proven, not a risk: no quoting exists anywhere in the path

Traced end to end. The local half verified in this tree: push_shell_argv_tokens
pushes each evaluated String verbatim and both exec branches call
Command::new(argv[0]).args(argv[1..]), so transport shell at this boundary is
DIRECT PROCESS EXECUTION -- no local shell, no shell_quote, no command-string
renderer. sshpass execvps unchanged. OpenSSH's client consumes -- as its own
option terminator and joins remaining argv with single literal spaces, no
escaping. OpenBMC's default server is Dropbear (corrected from sshd), whose
run_shell_command invokes the login shell with -c.

So a filter containing unquoted pipes arrives remotely as shell pipeline
operators and the jq program's argument boundary is gone. The code assumes
shell_parse(join(argv, ' ')) == argv, which holds only inside the portable-word
alphabet typed_argv_exec exists to bound; these filters are outside it.

Judgments split rather than lumped: boundary preservation Violates
(source-proven); deployed client, reachability and production manifestation
Unverified; Dropbear shell exec StronglySupported but unobserved on this
firmware. Enumerated saving conditions, none visible in the repo. Executed
control specified with jq -n so it cannot mutate BMC state, with the
unexpected-success branch treated as evidence for an unmodeled layer rather
than dismissed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Wave 0: the grammar's token stream survives as argument boundaries, proven by execution

The CLI serializer is not a second emitter. bound_tokens_source_text folds a
grammar-selected token sequence, resolves each token to its spelling, and joins
with target_text_seq -- concatenation. That join is where argument boundaries
die, and re-deriving them afterwards is what shell_quote is at 36 sites.

bound_tokens_cli_arguments is the SAME fold with the SAME spelling resolution
and a different join: one argument per token. Nothing about the grammar walk
changes; only whether the boundary survives.

EXECUTED RECEIPT, not a compile:
  cli_serializer_preserves_argument_boundaries  returned true
  text_serializer_loses_the_argument_boundary   returned true
  definitely_not_a_real_function                errored

Two tokens chosen as the smallest thing that can separate the carriers:
"--argjson" and "[1,2] | length". The second carries a space and a pipe, the
shape that loses its boundary at the ssh seam in the 17 remote jq rows. The CLI
carrier yields two arguments with the program intact as one; the text carrier
yields "--argjson[1,2] | length" with the boundary gone.

The third arm is why the first two are evidence. A compile-only probe would
false-green here: emit and serialize_target are fixed to Medium<String>, and
v1.04_infer explicit_return_conformance_note records that declared-return
conformance is judged only by the ground-kernel-scalar and
ground-element-collection discipline, so a structured carrier mismatch raises
no diagnostic. An entry returning ProcessExit exits 0 SILENTLY, which is
indistinguishable from never running -- the first run of this probe produced
exactly that empty rc=0 and proved nothing. Running the Bool-returning
assertions directly forces gunbc to print the value it got, and the
nonexistent-function control proves the harness reaches this file at all.

CliSurface and CliArgument are sole_constructor with NO exported mint.
TransportScript needs transport_script_seal because production modules must
build one; nothing outside this module has business constructing a CLI
argument, because an argument is a RESULT of the grammar fold, never an
authored value. So there is no admit_callers list to add a name to.

WHAT THIS DOES NOT YET PROVE, stated rather than implied: this is the CARRIER
half (the join), not the SEAM half. emit_cli_probe binding translate's output
to this serializer is not built, corpus-wide text byte-identity is not
measured, the TargetSurfaceSerializerUnwired refusal is declared but not
exercised, and no probe yet proves CliSurface itself is sealed -- dropping the
keyword would red nothing today. The five sole_constructor controls in
gunbc.guarantee_probe_corpus prove the LANGUAGE FEATURE against a fixture; what
is owed is one probe that THIS type uses it.

Design: docs/plans/cli-invocation-emission-design.md

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Delete the two unconsumed decls, and correct a sealing claim that was backwards

Review found target_surface_serializer_unwired_diagnostic and
cli_surface_argument_count had zero callers. Deleted rather than wired or
deferred: no consumer exists, wiring would mean inventing one, and deferring
leaves specification-without-execution in the tree with a promise attached.
Model just-in-time -- the refusal arm arrives with the code that can reach it.
The irony is recorded because it is the point: TargetSurfaceSerializerUnwired
existed so a missing serializer could not silently fall back to text, and it
landed unwired, which is exactly as inert as the fallback it was meant to
prevent. Confirmed inert by execution, not by inspection: both probe
assertions still return true after the deletion.

The larger correction is to the carrier comment. It claimed this seal was
STRONGER than TransportScript because there is no exported mint and therefore
no admit_callers roster to add a name to. That is backwards.
bound_tokens_cli_arguments is public and takes tokens, lex rules and binding
spellings from its CALLER, so any module can synthesize arbitrary content and
receive a sealed CliSurface. You cannot author the record; you can author its
contents. That is the mint-function hole gunbc.guarantee_probe_corpus already
enumerates as sole_ctor_mint_fn_hole_probe -- read three hours earlier, cited
as the reason not to re-prove the language feature, then reproduced.

TransportScript's seal is admit_callers-restricted to two named production
decls. This fold admits everyone. So the carrier is WEAKER, and the claim was
made, reviewed and corroborated once before anyone checked it.

Not closed in this commit, deliberately. The fix is to stop taking
caller-supplied grammar -- the fold reachable only already bound to a target
model, so the lex table is the target's -- and that shape depends on whether
the jq path consumes translate's target model or bypasses it. An admit_callers
roster now would admit only this probe, which is a wall around an empty room.
Dissolves with the wave that adds the first production consumer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Wave 0 corrected: group fragments into arguments, and stop proving a tautology

THE THEOREM I HAD BEEN ASSERTING WAS WRONG. Concatenation is not inherently
where CLI structure dies -- concatenation at the WRONG STRUCTURAL LEVEL is.
Within one argument concatenation is exactly right (["--color","=","never"] is
one argument --color=never; ["-","e","r"] is one argument -er). Across
arguments it destroys the boundary. So the algebra is nested, not flat:
fragments join WITHIN an argument, arguments stay separate BETWEEN.

THE OLD WITNESS PROVED A TAUTOLOGY. It supplied two tokens to a
one-token-one-argument fold and asserted two arguments came out, which chose
the argument split before the serializer ran. It established "one token
supplied, one argument retained" -- a restatement of the fold's own shape --
not "the grammar groups fragments into arguments". An approving review read it
as a positive claim plus a negative control, which is how a self-fulfilling
test passes for evidence.

THE NEW WITNESS CAN FAIL. Same three fragments, two groupings, executed:
  joined_fragments_render_one_argument        returned true   ["--color=never"]
  separated_fragments_render_three_arguments  returned true   ["--color","=","never"]
  both_groupings_flatten_to_the_same_text     returned true   "--color=never"
The third is the keystone: both groupings flatten to IDENTICAL text, so the
text carrier cannot distinguish them at all. Grouping is information the argv
carrier holds and text does not -- exactly what the 17 remote jq rows lose at
the ssh seam. Were grouping not load-bearing, arms one and two would agree.
The three function names do not exist in the parent commit, so their resolving
is itself the control that the new file reached the runner.

The inner join reuses bound_tokens_source_text rather than forking a second
concatenation: within an argument, the text fold is the correct tool, and
DESIGN section 2 says model once and derive.

ALSO CORRECTED: the comment claiming this "consumes what translate already
produced" was false -- the witness hand-constructs its tokens and nothing here
calls translate. It consumes the same ConcreteSyntaxToken representation the
existing target serializers use, which is the true and still-useful claim. And
probe_verdict() -> ProcessExit is DELETED: it exits 0 silently on success, the
exact false-green that made this probe's first run report nothing while
appearing to pass, and leaving that shape beside the corrected evidence is how
the trap gets re-sprung.

STILL OWED, unchanged: the mint hole. serialize_cli_arguments still takes
caller-supplied lex rules, so arbitrary content can still reach a sealed
CliSurface. The fix is to seal the INPUT (AdmittedCliInvocation) rather than
admit_callers the serializer, because listing every tool centrally would make
adding a tool a core edit -- anyone may call the serializer, nobody may forge
what it consumes. That needs the schema layer and lands with the first
consumer. Also owed: exact-type REDs against CliArgument/CliSurface
themselves, and tool: CliToolRef so tool identity stops being ambient.

Jq will NOT route through translate or TargetModel; emit_cli_probe is not to be
built. The surviving seam is the spelling algebra below them, which is the part
this wave actually found.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Wave 1A: jq semantic invocation layer, lowered to argv through the shared CLI surface

The domain module now states WHAT it wants of jq -- a program, an input, an output
encoding, an exit policy -- and the argv vector is derived from that, rather than being
the authority. Two-level derivation, so both defect classes are closed at their own
level: semantic property -> option identity (JqCliSelection) prevents OMISSION, and
option identity -> canonical spelling (bare name + cli_long_option_spelling) prevents
bespoke SPELLING. jq_option_long_name returns "raw-output", never "--raw-output": the
dashes belong to the grammar, not to the option's identity.

JqCliSelection is a coproduct rather than an Optional because "no option is required for
this semantic property" and "this property has no answer" are different states, and the
lane exists to stop collapsing exactly that kind of distinction.

The lowering REFUSES the axes with no live consumer yet -- bindings (the --argjson
vertical, landing with ObjectMapperServiceAt) and file input (the remote population) --
as typed, located refusals rather than a plausible guess.

Executed, on the real acceptance path (all nine return true; a nonexistent-function
control refuses with NoSuchFunction, so a silent no-run cannot read as a pass):
  W0  joined_fragments_render_one_argument
  W0  separated_fragments_render_three_arguments
  W0  both_groupings_flatten_to_the_same_text
  W0  keystone_flat_text_is_nonempty
  W1A sensor_invocation_lowers_to_exact_argv
  W1A stdin_content_is_absent_from_argv
  W1A exit_policy_perturbation_adds_the_exit_status_option
  W1A unlowered_bindings_refuse
  W1A unlowered_file_input_refuses

Three defects found and fixed getting there, each recorded rather than quietly patched:
a source annotation placed inside a declaration body (DESIGN 4c admits module-item grain
only); three stale call sites left when the Optional-returning selectors became
JqCliSelection; and a type mismatch at the stdin field, bisected remotely to
Present { value: ... } with the payload expression irrelevant -- a bound variable, a
renamed binding, a shorthand pattern and a bare literal all reproduce it while Absent
resolves. This uses the corpus's own String? sugar (625 existing optional fields). That
observation is recorded as MEASURED AND NOT DIAGNOSED in the design note, with a section
5 line-stop owed before anything in this lane relies on the distinction.

Nothing is cut over yet: no consumer is rewired and no transport argv is deleted. This
is the semantic layer plus its discriminating evidence, not the replacement.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Correct rung inflation in this lane's own authority: the CliSurface seal is on shape, not provenance

Section 9's table claimed forging a CliSurface is "structurally impossible now -- only the
row emitter, serializer and decoder may mint". That is false, and it is the exact failure
DESIGN 4b calls worse than sitting low: a carrier named for the top rung while occupying a
lower one, asserted here about this document's own subject.

sole_constructor closes the record literal and the cast. It says nothing about a public fold
taking caller-supplied inputs, and serialize_cli_arguments is precisely that -- public, and
accepting caller-supplied lex rules and fragments, so any module can obtain a well-typed
CliSurface carrying arbitrary text. The earlier claim in this lane that CliSurface was
therefore STRONGER than TransportScript had the comparison backwards: TransportScript's mint
is admit_callers-sealed to two named production declarations; CliSurface's is not sealed at
all.

The row is split, because one number for two populations was the error:
  forging by record literal or cast  -> structurally impossible (mechanism witnessed by the
                                       existing corpus sole-constructor-cross-module probes,
                                       deliberately not re-proved here -- that would be a
                                       second representation of one guarantee)
  minting content not derived from rows -> mitigatable only, no wall

Ceiling and trigger are now stated rather than implied. admit_callers on the serializer is
REFUSED on section 3 grounds: it would make v2.std.compilers.cli_surface name every tool
module that may emit a CLI, fusing dispatch into the interface -- the thing this lane exists
to keep peripheral. The wall belongs on the INPUT: a sealed AdmittedCliInvocation only a
tool's own row-derived lowering can produce. That is not built, and its mint's design is
genuinely open, since whatever seals it faces the same recursion one level up. Recorded as
open rather than improvised, since a fake wall here would be the inflation again.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Fix two stale claims in cli_surface's own mint-hole note, one of which had a trigger that could not close it

Surfaced by an approving review quoting the header back: it described the dissolve-on as
"first production consumer choosing the target-model path". Both halves of that were stale.

1. STALE SYMBOL. The note named the mint bound_tokens_cli_arguments, which no longer exists;
   it is serialize_cli_arguments. This is exactly the section 3 class -- a name-level claim a
   grep decides, sitting false in the file a reviewer reads to judge the seal.

2. AN ANSWERED QUESTION STILL BEING DEFERRED TO, and this is the substantive half. The note
   said the repair's shape "is decided by whether the jq path consumes translate's target model
   or bypasses it entirely". Wave 1A answered it by execution: jq BYPASSES it. The lowering
   builds CliArgumentSyntax from its own rows and never constructs a TargetModel, so "bind the
   fold to a target model so the lex table is the target's" is not merely undone -- it is
   unavailable, there being no target model on this path.

   The old trigger was therefore worse than vague: "the wave that adds the first production
   consumer" would have FIRED without closing the hole, retiring the obligation while the
   unrestricted mint stayed open.

The corrected repair is to seal the INPUT, not the fold: a sealed AdmittedCliInvocation only a
tool's own row-derived lowering can produce. admit_callers on the serializer stays refused on
section 3 grounds -- not because the roster would be short, but because it would make this std
module name every tool permitted to emit a CLI, fusing dispatch into the interface. The
dissolve-on is now that carrier, and provenance is stated as sitting at mitigatable meanwhile.

Verified still resolving after the edit (annotations are parsed, so a comment edit can break
the module): five representative Wave 0 and Wave 1A assertions re-run, all return true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Record the spelling-seam extraction: right finding, forbidden shape, corrected decomposition

The static-dependency finding stands. At execution grain the jq fold reaches no compiler
machinery; at dependency grain cli_surface imports target_model, whose closure carries
target-representation, host-runtime and node-query machinery. The property worth having is
not "nobody calls translate" but "this fold cannot acquire that dependency accidentally".

THE OBVIOUS REPAIR IS FORBIDDEN BY A RULING IN THE FILE IT WOULD EDIT. Extracting a shared
spell_concrete_syntax_fragments -> Outcome<String> and having the TargetText serializer wrap
its result is a String -> TargetText lift of an ALREADY-COMPOSED unit. target_model
target_text_carrier_scaffold_note (operator, 2026-07-15) places TargetText beside
bound_tokens_source_text precisely so that fold is carrier-native: the single String->carrier
introduction is text_atom applied to ONE grammar-classified token INSIDE the fold, the only
join is target_text_seq, the only exit is render_target_text, and it states there is
deliberately NO lift of a composed unit -- "that direction is the smuggle the wall closes."
I was one edit from dismantling a declared wall on a load-bearing file.

THE CORRECTED DECOMPOSITION IS BETTER ANYWAY. The shared authority is WHAT IS THIS TOKEN'S
SPELLING -- lex_rules_literal_for_class and bound_spelling_from_map, both token-grain -- not
HOW ARE SPELLINGS CONCATENATED. Concatenation is carrier-specific by construction: emitted
source composes through TargetText, an argv argument composes into a CliArgument, different
media. So the move is the token type plus the two token-grain lookups into
v2.std.compilers.concrete_syntax, with target_model importing them back and each carrier
keeping its own fold. No composed String is ever lifted, cli_surface stops importing
target_model, and one lookup authority still serves both.

RE-EXPORT IS MEASURED, NOT ASSUMED. A three-module probe showed a consumer importing a symbol
from a module that merely imported it resolves and executes. That alone proves nothing: this
resolver can bind by pool-membership coincidence (DESIGN Class B). The discriminating control
settles it -- importing the same symbol from a bystander module that never saw it REFUSES,
located, with the defining module still in the pool. Resolution is import-list-driven, so
target_model importing the seam back leaves its 167 other importers untouched.

NOT PERFORMED HERE. target_model is load-bearing and carries the ruling above, so the move is
its own increment under its own review rather than a rider on this one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Name the import jq was resolving by pool coincidence, and record the specimen

extdeps.tools.jq jq_option_canonical_spelling calls cli_long_option_spelling while the module's
import list named only CliArgumentSyntax, CliSurface and serialize_cli_arguments. The call
resolved anyway -- and all nine Wave 1A assertions passed -- because cli_surface was already in
the assembled closure via those three imports. Found by review, not by any control I had.

That is the Class B accidental coverage DESIGN's import-strip thread records as blocking all
further dag/** import stripping: the binding came from pool membership, not from the
bare-reference closure.

Note which control does NOT catch it, since I ran one an hour earlier and it proved a
neighbouring property. The bystander probe refuses a QUALIFIED import of a name a module does
not export. This is an UNIMPORTED BARE REFERENCE into a module present for other reasons.
Different mechanism, and only the second is silent.

Swept all four files of this lane rather than fixing the reported site alone: this was the only
real hit. concat is a registered host builtin (target_model does not import it either) and
`then` was a false positive from inside a jq program string literal.

Verified after the fix: five Wave 1A assertions re-run, all return true.

THE GENERAL DEFECT IS UNTOUCHED and is not this lane's to fix -- nothing refuses the next such
reference. The durable lesson is recorded in the design note: a green witness is not evidence
that a module's imports are complete.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Four review corrections, three of which my passing tests were concealing

All four raised by side-chat review of Wave 1A. Each was real; the notable part is that three
were invisible to a green assertion set.

1. THE FOLD WAS FAIL-OPEN ON A PATH TO Command::new. target_model bound_spelling_from_map
   answers an absent map entry with the binding SYMBOL'S OWN NAME rather than refusing.
   Defensible for compiler source text, where the symbol name is a legitimate rendering; for
   runtime CLI data it means a missing jq_program_text binding emits the literal argument
   "jq_program_text" -- fabricated plausible output (DESIGN section 5) that a process then runs.
   cli_surface now has its own CliArgument-native fold with required_bound_spelling, which
   refuses, typed and located.

   This also satisfies the carrier ruling rather than fighting it: the shared authority is
   TOKEN-GRAIN SPELLING, not sequence composition, so emitted source keeps composing through
   TargetText via text_atom/target_text_seq while an argv argument composes here, and no
   already-composed String is lifted into either carrier.

   PROVEN DISCRIMINATING, not assumed: a_bound_fragment_with_no_spelling_refuses returns true
   with the refusing fold and FALSE when the fallback is restored. Executed both ways.

2. THE PUBLIC RESULT DROPPED STDIN. jq_invocation_cli_arguments projected plan.arguments and
   discarded plan.stdin, so a jq program's input vanished at the module boundary. The witness
   could not catch it: "stdin does not appear in argv" is satisfied just as well by stdin being
   lost entirely -- a negative control that coexists with total loss is not evidence of routing.
   Adds sealed JqAdmittedProcessPlan { tool, surface, stdin } with both halves asserted, and it
   gives tool identity its first consumer so which binary runs stops being ambient.

3. THE REFUSAL CAUSE WAS ERASED. JqLoweringRefused carried a NonEmptyStr reason that
   jq_lowering_refused_diagnostic never read, collapsing both unlowered axes onto one identity
   while the witnesses asserted only a generic Rejected. Typed JqLoweringRefusal now projects
   distinct identities, asserted by three new witnesses.

4. The unlisted bare import fixed in the previous commit.

Fifteen assertions execute, all true. Deliberately NOT added: arity, repeatability and joining
discipline have no consumer. Placement does (jq_option_arguments orders options before the
program operand), but it belongs encoded structurally as options/operands on the future
AdmittedCliInvocation, not as a per-option enum on every row.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Update the entry-point claims those corrections just falsified

jq_invocation_process_plan became the complete result in the previous commit, which made three
statements stale in the same motion: jq.dag's header, cli_surface's containment sentence, and
section 9 of the design note all said jq_invocation_cli_arguments was the single public entry.

The argv-only projection stays beside it, because the boundary witness asserts over it directly.
What is now written down is why a handler must NOT take it: recovering stdin would mean reopening
the JqInvocation, which gives the process projection two authorities -- the thing the sealed plan
exists to prevent.

This is the fourth stale-claim fix in this lane and they share one shape: the mechanism changed
and the sentence describing it did not. Verified after the edit, since annotations are parsed and
a comment change can break a module.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Name two more imports jq was resolving by pool coincidence (review 53669)

jq_invocation_process_plan used bind_outcome and outcome_accepted with neither in the module's
v2.std.diagnostic import list. The finding is correct and is fixed here.

THE REVIEW'S STATED CONSEQUENCE IS NOT CORRECT, and the difference matters more than the fix.
It said "as written this file will not resolve". The file resolves, and
stdin_survives_lowering_into_the_process_plan executes green THROUGH the affected function,
because v2.std.diagnostic is already in the closure via other imports. A reviewer predicting a
resolution failure would be refuted by running it and might then discard a real finding as a
false positive. The accurate statement: the references bind by pool membership, and nothing in
the tree reports it -- not the resolver, not CI, not a green witness.

THIS IS THE SECOND OCCURRENCE IN THIS LANE, in code written AFTER the class was documented two
commits ago. The cause is procedural and worth recording: the unimported-reference sweep had
been run and was clean, then jq_invocation_process_plan was added and the sweep was not re-run.
A one-time audit cannot close a class whose defect is invisible by construction; the sweep
belongs after every addition. Re-run across all four files of the lane, now clean (concat is a
registered host builtin; `then` is a false positive from inside a jq program string literal).

Six assertions re-run after the fix, all true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Delete five declarations sitting ahead of their consumers (side-chat review)

Verified before removing, since "unused" is a claim about the whole tree:

  jq_option_for_binding      1 reference -- its own definition. Dead.
  JqCliOptionArgJson         reachable ONLY from that dead function, plus exhaustive match
  JqCliOptionArg             arms and lex rows for options nothing can select.
  jq_option_short_name       no consumer.
  cli_short_option_spelling  no consumer.

The binding-option rows are the interesting ones. jq_invocation_lower REFUSES any non-empty
bindings, so nothing could ever select them: a typed refusal already stood where those rows
implied a capability. Keeping them would have been a second answer to a question the refusal
already answers -- and they return with the --argjson vertical that earns them.

The long-option renderer's comment now says why only the long form is modeled: POSIX guideline
3 is cited in the design note, but a citation is not a consumer, and a rule nothing calls cannot
be shown to be right.

This is the third appearance of this class in this lane. Review caught two unwired declarations
earlier, I deleted them and wrote down the principle, and then authored five more. Stating the
principle has not prevented violating it; the mechanical sweep is what catches it, and it now
runs after every addition rather than once.

It also matters beyond tidiness. Unconsumed rows in a replacement Y are how a migration
accumulates authority before it removes any (DESIGN section 3), and this lane's displacement
numerator is still 0 of 28.

Fifteen assertions re-run after the deletions: 15 true, 0 false. The exhaustive-match arms were
the plausible breakage and did not break.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* BLOCKER, proven by execution: the argv transport silently joins computed argument lists

A List<String> built by folding is CONCATENATED into one argv word. The identical list written
as a literal is SPLICED. Same declared type, same elements, same handler, two different
processes.

RECEIPT, through a real jq handler:

  arguments = ["--raw-output", "."]        literal  -> exit 0   (jq ran; two argv words)
  arguments = fold_list(... same two ...)  folded   -> exit 2
      jq: Unknown option --raw-output.

and from the first wet run of the real vertical, three lowered arguments arriving as one:

  $ jq --raw-output--exit-status.missing   (exit=2)

MECHANISM. v1_interpreter.rs push_shell_argv_tokens: Value::List splices each item, but
Value::Variant tries value_as_host_string FIRST, which walks a free monoid and concatenates it
into a single String pushed as one argv word; only on None does it fall through to
free_monoid_to_vec and splice. A folded list is monoid-encoded with all-Str elements, so the
concatenating reader wins. gunbc.WitnessBin.Run escapes this only because its args is authored
as a literal at each call site.

INDEPENDENTLY ATTACKED. An outside reviewer tried to refute it and failed: the source matches
the reading, and the collapse happens BEFORE Command::args, ruling out a downstream shell or
SSH join. Three confirmations from different directions.

NEITHER OBVIOUS REPAIR IS CORRECT. Reordering the arms splices this case but SHREDS a modeled
String, because a String is itself a monoid here -- both readings succeed on a monoid of Str,
and the runtime cannot separate "list of arguments" from "string assembled from pieces". The
disambiguator is the declared type, erased at that seam: the same missing application-argument
typechecking target_text_carrier_scaffold_note names as the trigger for every type-based
construction guarantee at a call boundary. Hand-authoring literal argv in the handler defeats
row-derived lowering and leaves the next caller silently joined -- the workaround shape section
5 treats as a line-stop.

WHY NO CODE LANDS WITH THIS. The recut's handler, JqProcessInput, JqProcessObservation and
sealed-plan executor are built and resolve, but they are unconsumed AND blocked: no consumer can
migrate onto them without silently destroying argument boundaries. Landing them would bank
exactly the unconsumed replacement surface this lane has spent the day deleting. They are held
out of tree until the blocker is decided.

THE IRONY IS THE POINT. This lane exists because argv arrays weld argument boundaries into
opaque strings. The substrate's own argv transport does that, silently, one layer below --
Wave 0's witness asserts fragments concatenate WITHIN an argument and never ACROSS, and the
transport violates precisely that assertion.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Correct the blocker's conclusion: a construction exists, it is not blocked on argument typechecking

The previous commit's DIAGNOSIS survived independent adversarial review -- the reviewer traced
build_service_param_env (clones call arguments, no conformance check), dispatch_shell, and
Command::new(&argv[0]).args(&argv[1..]), confirming the vector is malformed before Command sees
it, so no downstream join can explain the observation. The refusal to reorder the branches was
upheld for the reason given.

ITS CONCLUSION WAS WRONG. I wrote that neither obvious repair is correct and the cut is blocked
pending application-argument typechecking. There is a third repair, and the counter-evidence is
already in tree: OperationInputValue = InputText | InputTextList carries tagged list intent, and
its realization converts that tag into a native Value::List via free_monoid_to_vec + list_value.
Tagged intent to native list is proven possible today without global typechecking.

The deeper correction is the one I missed. Even fully typechecked, List<String> still does not
say whether a collection becomes several argv words, one JSON argument, a comma-joined option
value, or repeated option/value groups. That is a TRANSPORT ROLE, not a data type. The missing
fact must be modeled, not inferred from runtime encoding.

The construction: a sealed ShellArgvExpansion { surface: CliSurface } plus an interpreter branch
ahead of the generic heuristic that requires the nominal CliSurface, iterates its arguments, and
pushes exactly one host word per CliArgument. It carries CliSurface rather than List<String> so
the payload cannot be dynamically ambiguous -- a modeled string cannot impersonate a list of
nominal CliArgument records -- and value_as_host_string is then applied only to one admitted
argument's text, where concatenation is correct. Wave 0's theorem enforced at the host edge.

Also recorded: the six repairs that must NOT land, each with its reason, including accepting both
a raw List<String> and the explicit carrier -- two authorities with the unsafe one still reachable.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Wave 1B: cut the first argv site over to the jq invocation layer, and make the exit code decodable

Deletes openbmc.JsonProjection.SensorIntegerValue -- transport argv, `success: Bool`
output and all -- and routes its two consumers through one shared function that states
what it wants extracted and never spells a flag, an option, an argument position or
argv[0]. The domain authors zero argv after this cut.

Carrier, at the host edge:

  ProcessArgvExpansion { surface: CliSurface }   sole_constructor

with the seed realization in v1_interpreter. It exists because a computed argument
vector was losing its argument boundaries: a folded List<String> is monoid-encoded, and
push_shell_argv_tokens tries value_as_host_string (which walks the monoid and
CONCATENATES) before free_monoid_to_vec (which splices), so a correctly-lowered
three-argument vector reached a real process as `jq --raw-output--exit-status.missing`,
exit 2. Literal lists escape only because they keep their native representation. The
carrier states the transport ROLE that List<String> cannot: iterate across arguments,
concatenate within one. Empty arguments are preserved (dropping one changes arity) and
an embedded NUL refuses with the argv position named, rather than reaching spawn as an
errno-shaped error naming neither.

Named ProcessArgvExpansion, not Shell: the realization is
Command::new(&argv[0]).args(&argv[1..]) -- no shell, no word splitting, no quoting
layer. Naming it for the `transport shell` keyword would name it after the surface DSL
rather than the boundary (S3).

The exit code now travels with its contract. JqAdmittedProcessPlan carries exit_policy
and jq_classify_observation is the only reader of an exit code, returning
Present | Absent | Refused. The sensor decoder previously mapped every nonzero exit to a
refusal -- correct under JqProgramExit, silently wrong under JqLastResultExit, where jq
documents exit 1 as a false-or-null last output (a value) and exit 4 as absence.
Changing the policy would have left the decoder answering the old contract: the
declaration edited while the realization goes on lying (S5).

Executed evidence:

  bmc_typed_operations         29/29   (2 migrated onto the typed outcome, 1 newly stateable)
  jq_invocation_lowering        9/9    lowering
                                5/5    exit-policy classification, incl. the row a
                                       policy-blind decoder cannot satisfy: exit 1 is a
                                       refusal under one policy and a value under the other
  bmc_fan_converge              duty_curve pass
  process_argv_expansion_receipt PASS  real jq, exit 0 reachable only with two argv words

Not claimed: the splice defect is repaired at ONE seam, not closed as a class -- 21
operations still splice a declared List through the guessing path. The remaining
JsonProjection operations are unmigrated and two need --argjson lowering, which is
unbuilt. No negative falsifier yet proves a REST path reaches none of these carriers.
The domain still authors one jq program row (design note S12: mitigatable, no wall,
dissolution trigger recorded -- the terminal shape is a modeled JSON projection of which
jq is one realization).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Rename the witness-local ExpectedOutcome: it collided with gunbc.output_policy and red a file this branch never touched

CI caught what every local run missed. The jq witness declared

  type ExpectedOutcome = ExpectPresent | ExpectAbsent | ExpectRefused

and gunbc.output_policy already declares that name (ExpectSuccess | ExpectFailure |
OutcomeIsData) -- the carrier the interpreter's expectation frontier consumes. The second
declaration did not shadow the first; it made the PRE-EXISTING bare reference in
dag/test/claim/output_policy_witness_test.dag:92 unresolvable, so the failure landed in a
file that references none of this branch's symbols and that this branch never modified.

Renamed to JqOutcomeExpectation, with the reason recorded on the declaration so it does
not get renamed back.

WHY NO LOCAL RUN CAUGHT IT: bare-reference resolution is corpus-global, but a per-file
`gunbc run` loads only that file's closure, so a new top-level name can red a file no
closure of mine would ever load. A per-file run and the required floor are different
universes and only the floor is the acceptance path -- reporting the first as though it
were the second is rung inflation against a declared boundary (S4b), which the design
note states as a rule about other people's claims and which I then committed against my
own change.

Two mechanical checks adopted, recorded in the note (S14), because the hand-authored
version of this has now failed three times in this lane -- each time with a sound
mechanism and an AUTHORED denominator:

  # every top-level name the branch ADDS, taken from the diff, not from memory
  git diff main...HEAD -- '*.dag' | grep "^+" \
    | grep -oE "^\+\s*(type|fn|data)\s+[A-Za-z_][A-Za-z0-9_]*" | awk '{print $NF}' | sort -u
  # each must have exactly ONE declaration corpus-wide

  # and run what CI runs, before pushing
  claim_executor --required-floor --source-root dag --source-root src/v2

The first check now reports zero collisions across all 82 names this branch adds.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Admit the wet argv receipt properly: excluded from hermetic discovery, enrolled as a wet entry

The floor ran 9201 witnesses with one failure, and it was this receipt:

  FAIL test.manual.process_argv_expansion_receipt.case4_expansion_carrier_splices
    hermetic mode: no mock_response for operation RunWithStdin -- refusing to fabricate Unit

The refusal is correct. case4 dispatches a real jq, the hermetic envelope has no mock
for that operation, and it refuses rather than skipping -- one refusing member fails the
run.

MOCKING IS NOT THE REPAIR, for the reason gunbc.ci_layer_roots already records against
the stage0 rows: this witness's entire content is that a real jq exits 0 only when it
receives TWO argv words instead of one concatenated word. A mocked RunWithStdin lets it
pass with no process running -- a green that cannot fail, asserting nothing about the
boundary defect it exists to detect. That approach was tried and reverted elsewhere in
the corpus; this row does not retry it.

TWO ROWS, because they answer different questions (DESIGN 'witness cost derives from
purpose', operator ruling 2026-08-04):

  WitnessExclusionRow          keeps it off a hermetic batch it cannot pass
  bin_witness_wet_entries      gives it an executing consumer

Exclusion alone would be deletion of the evidence with the source file retained, which
is the exact specimen that ruling was written from. Both rows land together.

Path decided nothing: the file sits under dag/test/manual/ and was swept into unshrunk
discovery anyway -- the same ruling's point that a directory cannot answer an admission
question.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Classify the wet receipt row BinWitnessWet, not OfflineLocalRecipe

Caught before CI ran it, by reading the reconciliation witness the roster answers to
rather than copying the shape of a neighbouring row.

The two classifications are not interchangeable labels; they project different claims:

  BinWitnessWet      -> SchedulingEnrolled
  OfflineLocalRecipe -> SchedulingDark

This receipt IS enrolled in bin_witness_wet_entries and does run per-PR, so the offline
label would have declared a running witness dark -- understating its own coverage in the
carrier whose entire job is to report coverage honestly. It is also the arm DESIGN's
witness-cost ruling retired: a broad offline path verdict accepted unconditionally is
precisely the admission defect that ruling was written from, and I reached for it while
quoting that same ruling one commit earlier.

BinWitnessWet is additionally the arm held to account -- the reconciliation witness reds
an unbacked BinWitnessWet row, and this one is backed by the entry it names.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Exclude the wet receipt through the mechanism the floor actually consults, and declare the coverage gap

The previous fix did not work and the CI receipt says why: modules_excluded stayed at 2
and the same witness failed identically. run_required_floor calls
prepare_repository_once(source_roots, &floor_prepared_subject_exclusions()) -- a
hardcoded Rust list, which is exactly those 2 entries -- and consults nothing else. The
rows I added to gunbc.ci_layer_roots were inert:

  witness_exclusion_frontier   feeds witness_admission_* paths, not the floor
  bin_witness_wet_entries      feeds wet batches that died with the floor cut

Both are reverted. A row in a roster with no live consumer is
specification-without-execution, and I had additionally asserted in a commit message that
they would take effect -- a claim about a mechanism whose caller I never traced. The
BinWitnessWet reclassification was the same error compounded: the one host projection
that does read those rows filters on OfflineLocalRecipe, so "correcting" the
classification moved the row further from the only consumer it had.

The file is now named in floor_prepared_subject_exclusions, beside the existing
test/manual/ precedent.

WHAT THIS BUYS AND WHAT IT DOES NOT. It buys a green floor. It does not buy coverage:
there is no wet lane in CI at all -- the falsifier and wet batches were deleted with the
floor cut, and v2.workflow.required_floor defers wet lanes until the question can be
"asked against a live consumer". So the claim is recorded as UNEXECUTED-IN-CI with its
local recipe and a re-enrollment trigger, not dressed up as an enrollment. Declaring a
counted gap is the honest rung; claiming an executing consumer for a witness nothing runs
would be the inflation DESIGN 4b names as worse than sitting low.

Mocking remains refused: case4 exists to prove a real jq exits 0 only on two argv words,
and a mocked dispatch passes it with no process running.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>